(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ ?3 : ∥ a ∥ ?4 : ∥ a ∥ ?5 : ∥ b ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
((last . 2) . (agda2-make-case-action '("h0 = even-0" "h0 = even-s (odd-s h0)")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
((last . 2) . (agda2-make-case-action '("map f [] = []" "map f (x ∷ x₁) = f x ∷ map f x₁")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
((last . 2) . (agda2-make-case-action '("lookup zero (cons x x₁) = x" "lookup (succ x) (cons x₁ x₂) = lookup x x₂" "lookup zero (cons x x₁) = x" "lookup (succ x) (cons x₁ x₂) = lookup x x₂")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
(agda2-give-action 3 "eval σ e (eval σ e₁)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ ?4 : ∥ a ∥ ?5 : ∥ b ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2 4 5)))
(agda2-give-action 4 "lookup' x σ")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ ?5 : ∥ b ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2 5)))
(agda2-give-action 5 "eval (cons x σ) e")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2)))
